<HTML><HEAD>
<META NAME="copyright" CONTENT="Copyright (c) 1986-2008, Eiffel Software and others">
<META NAME="license" CONTENT="Eiffel Forum License v2 (see forum.txt)">
<META NAME="description" CONTENT="Sequences of 8-bit characters, accessible through integer indices in a contiguous range.">
<META NAME="library" CONTENT="Free implementation of ELKS library">
<META NAME="keywords" CONTENT="Eiffel class">
<META NAME="keywords" CONTENT="Eiffel class">
<TITLE>string_8 Flat contracts</TITLE></HEAD>
<BODY BGCOLOR="white">
<P ALIGN="CENTER">Automatic generation produced by ISE Eiffel</P>
<PRE><TABLE BORDER="1" ALIGN="CENTER"><TR><TD><A HREF="../class_list.html">Classes</A></TD><TD><A HREF="../cluster_list.html">Clusters</A></TD><TD><A HREF="../cluster_hierarchy.html">Cluster hierarchy</A></TD><TD><A HREF="string_8_chart.html">Chart</A></TD><TD><A HREF="string_8_links.html">Relations</A></TD><TD>Flat contracts</TD></TR></TABLE><B>indexing</B>
    description: "[
        Sequences of 8-bit characters, accessible through integer indices
        in a contiguous range.
    ]"
    library: "Free implementation of ELKS library"
    copyright: "Copyright (c) 1986-2008, Eiffel Software and others"
    license: "Eiffel Forum License v2 (see forum.txt)"
    date: "$Date: 2008-08-12 22:46:45 +0200 (Tue, 12 Aug 2008) $"
    revision: "$Revision: 186 $"

<B>class</B> <B>interface</B>
    <A HREF="../base/string_8_flatshort.html">STRING_8</A>


<B>create</B> 
    <A NAME="f_make"><A HREF="../base/readable_string_8_flatshort.html#f_make">make</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Allocate space for at least </FONT>`n'<FONT COLOR="red"> characters.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            non_negative_size: n &gt;= 0
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            empty_string: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0
            area_allocated: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= n
</A>
    <A NAME="f_make_empty"><A HREF="../base/readable_string_8_flatshort.html#f_make_empty">make_empty</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create empty string.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0
            area_allocated: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= 0
</A>
    <A NAME="f_make_filled"><A HREF="../base/readable_string_8_flatshort.html#f_make_filled">make_filled</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create string of length </FONT>`n'<FONT COLOR="red"> filled with </FONT>`c'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            valid_count: n &gt;= 0
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            count_set: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = n
            area_allocated: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= n
            filled: <A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c) = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_make_from_string"><A HREF="../base/readable_string_8_flatshort.html#f_make_from_string">make_from_string</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialize from the characters of </FONT>`s'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            string_exists: s /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            not_shared_implementation: <B>Current</B> /= s <B>implies</B> <B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_shared_with">shared_with</A> (s)
            initialized: <A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (s)
</A>
    <A NAME="f_make_from_c"><A HREF="../base/string_8_flatshort.html#f_make_from_c">make_from_c</A> (c_string: <A HREF="../base/pointer_flatshort.html">POINTER</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialize from contents of </FONT>`c_string'<FONT COLOR="red">,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> a string created by some C function</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            c_string_exists: c_string /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
</A>
    <A NAME="f_make_from_cil"><A HREF="../base/string_8_flatshort.html#f_make_from_cil">make_from_cil</A> (a_system_string: <A HREF="../base/system_string_flatshort.html">SYSTEM_STRING</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialize Current with </FONT>`a_system_string'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_dotnet: {<A HREF="../base/platform_flatshort.html">PLATFORM</A>}.<A HREF="../base/platform_flatshort.html#f_is_dotnet">is_dotnet</A>
</A>
<B>convert</B>
    <A HREF="../base/string_8_flatshort.html#f_make_from_cil">make_from_cil</A>: {<A HREF="../base/system_string_flatshort.html">SYSTEM_STRING</A>},
    <A HREF="../base/string_8_flatshort.html#f_make_from_cil">make_from_cil</A> ({<A HREF="../base/system_string_flatshort.html">SYSTEM_STRING</A>}),
    <A HREF="../base/string_8_flatshort.html#f_make_from_cil">make_from_cil</A>: {<A HREF="../base/readable_string_32_flatshort.html">READABLE_STRING_32</A>,
    <A HREF="../base/string_32_flatshort.html">STRING_32</A>}

<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialization</FONT>

    <A NAME="f_adapt"><A HREF="../base/string_8_flatshort.html#f_adapt">adapt</A> (s: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Object of a type conforming to the type of </FONT>`s'<FONT COLOR="red">,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> initialized with attributes from </FONT>`s'
        <B>ensure</B>
            adapt_not_void: <B>Result</B> /= <B>Void</B>
            shared_implementation: <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_shared_with">shared_with</A> (s)
</A>
    <A NAME="f_from_c"><A HREF="../base/string_8_flatshort.html#f_from_c">from_c</A> (c_string: <A HREF="../base/pointer_flatshort.html">POINTER</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Reset contents of string from contents of </FONT>`c_string'<FONT COLOR="red">,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> a string created by some C function.</FONT>
        <B>require</B>
            c_string_exists: c_string /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
        <B>ensure</B>
            no_zero_byte: <B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> ('%U')
</A>
    <A NAME="f_from_c_substring"><A HREF="../base/string_8_flatshort.html#f_from_c_substring">from_c_substring</A> (c_string: <A HREF="../base/pointer_flatshort.html">POINTER</A>; start_pos, end_pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Reset contents of string from substring of </FONT>`c_string'<FONT COLOR="red">,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> a string created by some C function.</FONT>
        <B>require</B>
            c_string_exists: c_string /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
            start_position_big_enough: start_pos &gt;= 1
            end_position_big_enough: start_pos &lt;= end_pos + 1
        <B>ensure</B>
            valid_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = end_pos - start_pos + 1
</A>
    <A NAME="f_make"><A HREF="../base/readable_string_8_flatshort.html#f_make">make</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Allocate space for at least </FONT>`n'<FONT COLOR="red"> characters.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            non_negative_size: n &gt;= 0
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            empty_string: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0
            area_allocated: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= n
</A>
    <A NAME="f_make_empty"><A HREF="../base/readable_string_8_flatshort.html#f_make_empty">make_empty</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create empty string.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0
            area_allocated: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= 0
</A>
    <A NAME="f_make_filled"><A HREF="../base/readable_string_8_flatshort.html#f_make_filled">make_filled</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create string of length </FONT>`n'<FONT COLOR="red"> filled with </FONT>`c'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            valid_count: n &gt;= 0
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            count_set: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = n
            area_allocated: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= n
            filled: <A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c) = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_make_from_c"><A HREF="../base/string_8_flatshort.html#f_make_from_c">make_from_c</A> (c_string: <A HREF="../base/pointer_flatshort.html">POINTER</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialize from contents of </FONT>`c_string'<FONT COLOR="red">,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> a string created by some C function</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            c_string_exists: c_string /= <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>
</A>
    <A NAME="f_make_from_cil"><A HREF="../base/string_8_flatshort.html#f_make_from_cil">make_from_cil</A> (a_system_string: <A HREF="../base/system_string_flatshort.html">SYSTEM_STRING</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialize Current with </FONT>`a_system_string'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_dotnet: {<A HREF="../base/platform_flatshort.html">PLATFORM</A>}.<A HREF="../base/platform_flatshort.html#f_is_dotnet">is_dotnet</A>
</A>
    <A NAME="f_make_from_string"><A HREF="../base/readable_string_8_flatshort.html#f_make_from_string">make_from_string</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Initialize from the characters of </FONT>`s'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            string_exists: s /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            not_shared_implementation: <B>Current</B> /= s <B>implies</B> <B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_shared_with">shared_with</A> (s)
            initialized: <A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (s)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Access</FONT>

    <A NAME="f_area"><A HREF="../base/string_8_flatshort.html#f_area">area</A>: <A HREF="../base/special_flatshort.html">SPECIAL</A> [<A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>]</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Storage for characters</FONT>

    <A NAME="f_code"><A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Numeric code of character at position </FONT>`i'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            valid_index: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
</A>
    <A NAME="f_false_constant"><A HREF="../base/readable_string_8_flatshort.html#f_false_constant">false_constant</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A> <B>is</B> "false"</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Constant string "false"</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>

    <A NAME="f_fuzzy_index"><A HREF="../base/readable_string_8_flatshort.html#f_fuzzy_index">fuzzy_index</A> (other: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>; start: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>; fuzz: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Position of first occurrence of </FONT>`other'<FONT COLOR="red"> at or after </FONT>`start'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> with 0..</FONT>`fuzz'<FONT COLOR="red"> mismatches between the string and </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if there are no fuzzy matches</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            other_exists: other /= <B>Void</B>
            other_not_empty: <B>not</B> other.<A HREF="../base/readable_string_general_flatshort.html#f_is_empty">is_empty</A>
            start_large_enough: start &gt;= 1
            start_small_enough: start &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            acceptable_fuzzy: fuzz &lt;= other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_generating_type"><A HREF="../base/any_flatshort.html#f_generating_type">generating_type</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Name of current object's generating type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (type of which it is a direct instance)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            generating_type_not_void: <B>Result</B> /= <B>Void</B>
            generating_type_not_empty: <B>not</B> <B>Result</B>.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_generator"><A HREF="../base/any_flatshort.html#f_generator">generator</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Name of current object's generating class</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (base class of the type of which it is a direct instance)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            generator_not_void: <B>Result</B> /= <B>Void</B>
            generator_not_empty: <B>not</B> <B>Result</B>.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_hash_code"><A HREF="../base/readable_string_8_flatshort.html#f_hash_code">hash_code</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Hash code value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/hashable_flatshort.html">HASHABLE</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/hashable_flatshort.html">HASHABLE</A>
            good_hash_value: <B>Result</B> &gt;= 0
</A>
    <A NAME="f_index_of"><A HREF="../base/readable_string_8_flatshort.html#f_index_of">index_of</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; start_index: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Position of first occurrence of </FONT>`c'<FONT COLOR="red"> at or after </FONT>`start_index'<FONT COLOR="red">;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if none.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            start_large_enough: start_index &gt;= 1
            start_small_enough: start_index &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            valid_result: <B>Result</B> = 0 <B>or</B> (start_index &lt;= <B>Result</B> <B>and</B> <B>Result</B> &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)
            zero_if_absent: (<B>Result</B> = 0) = <B>not</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c)
            found_if_present: <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c) <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (<B>Result</B>) = c
            none_before: <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c) <B>implies</B> <B>not</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <B>Result</B> - 1).<A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c)
</A>
    <A NAME="f_index_of_code"><A HREF="../base/readable_string_general_flatshort.html#f_index_of_code">index_of_code</A> (c: <B>like</B> <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A>; start_index: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Position of first occurrence of </FONT>`c'<FONT COLOR="red"> at or after </FONT>`start_index'<FONT COLOR="red">;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if none.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            start_large_enough: start_index &gt;= 1
            start_small_enough: start_index &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            valid_result: <B>Result</B> = 0 <B>or</B> (start_index &lt;= <B>Result</B> <B>and</B> <B>Result</B> &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)
            zero_if_absent: (<B>Result</B> = 0) = <B>not</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_general_flatshort.html#f_has_code">has_code</A> (c)
            found_if_present: <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_general_flatshort.html#f_has_code">has_code</A> (c) <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (<B>Result</B>) = c
            none_before: <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_general_flatshort.html#f_has_code">has_code</A> (c) <B>implies</B> <B>not</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <B>Result</B> - 1).<A HREF="../base/readable_string_general_flatshort.html#f_has_code">has_code</A> (c)
</A>
    <A NAME="f_item"><A HREF="../base/string_8_flatshort.html#f_item">item</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A> <B>assign</B> <A HREF="../base/string_8_flatshort.html#f_put">put</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Character at position </FONT>`i'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><FONT COLOR="red"> as synonym of </FONT><B>infix</B> "@"<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/to_special_flatshort.html">TO_SPECIAL</A>
            valid_index: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/table_flatshort.html">TABLE</A>
            valid_key: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            <B>True</B>
</A>
    <A NAME="f_item_code"><A HREF="../base/readable_string_8_flatshort.html#f_item_code">item_code</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Numeric code of character at position </FONT>`i'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            index_small_enough: i &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            index_large_enough: i &gt; 0
</A>
    <A NAME="f_last_index_of"><A HREF="../base/readable_string_8_flatshort.html#f_last_index_of">last_index_of</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; start_index_from_end: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Position of last occurrence of </FONT>`c'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if none</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            start_index_small_enough: start_index_from_end &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            start_index_large_enough: start_index_from_end &gt;= 1
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            last_index_of_non_negative: <B>Result</B> &gt;= 0
            correct_place: <B>Result</B> &gt; 0 <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (<B>Result</B>) = c
</A>
    <A NAME="f_shared_with"><A HREF="../base/readable_string_8_flatshort.html#f_shared_with">shared_with</A> (other: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does string share the text of </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_string"><A HREF="../base/readable_string_8_flatshort.html#f_string">string</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New STRING_8 having same character sequence as </FONT>`Current'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            string_not_void: <B>Result</B> /= <B>Void</B>
            string_type: <B>Result</B>.<A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (<B>create</B> {<A HREF="../base/string_8_flatshort.html">STRING_8</A>}.<A HREF="../base/readable_string_8_flatshort.html#f_make_empty">make_empty</A>)
            first_item: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>implies</B> <B>Result</B>.<A HREF="../base/string_8_flatshort.html#f_item">item</A> (1) = <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1)
            recurse: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 1 <B>implies</B> <B>Result</B>.<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_string">string</A>)
</A>
    <A NAME="f_string_representation"><A HREF="../base/readable_string_8_flatshort.html#f_string_representation">string_representation</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Similar to </FONT><A HREF="../base/readable_string_8_flatshort.html#f_string">string</A><FONT COLOR="red"> but only create a new object if </FONT>`Current'<FONT COLOR="red"> is not of dynamic type </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            result_not_void: <B>Result</B> /= <B>Void</B>
            correct_type: <B>Result</B>.<A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (<B>create</B> {<A HREF="../base/string_8_flatshort.html">STRING_8</A>}.<A HREF="../base/readable_string_8_flatshort.html#f_make_empty">make_empty</A>)
            first_item: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>implies</B> <B>Result</B>.<A HREF="../base/string_8_flatshort.html#f_item">item</A> (1) = <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1)
            recurse: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 1 <B>implies</B> <B>Result</B>.<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_string">string</A>)
</A>
    <A NAME="f_substring_index"><A HREF="../base/readable_string_8_flatshort.html#f_substring_index">substring_index</A> (other: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>; start_index: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Index of first occurrence of other at or after start_index;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if none</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            other_not_void: other /= <B>Void</B>
            valid_start_index: start_index &gt;= 1 <B>and</B> start_index &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            valid_result: <B>Result</B> = 0 <B>or else</B> (start_index &lt;= <B>Result</B> <B>and</B> <B>Result</B> &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1)
            zero_if_absent: (<B>Result</B> = 0) = <B>not</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_has_substring">has_substring</A> (other)
            at_this_index: <B>Result</B> &gt;= start_index <B>implies</B> other.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (<B>Result</B>, <B>Result</B> + other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 1))
            none_before: <B>Result</B> &gt; start_index <B>implies</B> <B>not</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, <B>Result</B> + other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 2).<A HREF="../base/readable_string_8_flatshort.html#f_has_substring">has_substring</A> (other)
</A>
    <A NAME="f_substring_index_in_bounds"><A HREF="../base/readable_string_8_flatshort.html#f_substring_index_in_bounds">substring_index_in_bounds</A> (other: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>; start_pos, end_pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Position of first occurrence of </FONT>`other'<FONT COLOR="red"> at or after </FONT>`start_pos'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> and to or before </FONT>`end_pos'<FONT COLOR="red">;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 0 if none.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            other_nonvoid: other /= <B>Void</B>
            other_notempty: <B>not</B> other.<A HREF="../base/readable_string_general_flatshort.html#f_is_empty">is_empty</A>
            start_pos_large_enough: start_pos &gt;= 1
            start_pos_small_enough: start_pos &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            end_pos_large_enough: end_pos &gt;= start_pos
            end_pos_small_enough: end_pos &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            correct_place: <B>Result</B> &gt; 0 <B>implies</B> other.<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (<B>Result</B>, <B>Result</B> + other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 1))
</A>
    <A NAME="f_true_constant"><A HREF="../base/readable_string_8_flatshort.html#f_true_constant">true_constant</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A> <B>is</B> "true"</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Constant string "true"</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>

    <A NAME="f_infix "@""><B>infix</B> "@" (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A> <B>assign</B> <A HREF="../base/string_8_flatshort.html#f_put">put</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Character at position </FONT>`i'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/string_8_flatshort.html#f_item">item</A><FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/to_special_flatshort.html">TO_SPECIAL</A>
            valid_index: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/table_flatshort.html">TABLE</A>
            valid_key: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            <B>True</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Measurement</FONT>

    <A NAME="f_additional_space"><A HREF="../base/resizable_flatshort.html#f_additional_space">additional_space</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Proposed number of additional items</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A>
            at_least_one: <B>Result</B> &gt;= 1
</A>
    <A NAME="f_capacity"><A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Allocated space</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/bounded_flatshort.html">BOUNDED</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            capacity_non_negative: <B>Result</B> &gt;= 0
</A>
    <A NAME="f_count"><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Actual number of characters making up the string</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>

    <A NAME="f_growth_percentage"><A HREF="../base/resizable_flatshort.html#f_growth_percentage">growth_percentage</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 50</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Percentage by which structure will grow automatically</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A><FONT COLOR="red">)</FONT>

    <A NAME="f_index_set"><A HREF="../base/readable_string_8_flatshort.html#f_index_set">index_set</A>: <A HREF="../base/integer_interval_flatshort.html">INTEGER_INTERVAL</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Range of acceptable indexes</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            not_void: <B>Result</B> /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            index_set_not_void: <B>Result</B> /= <B>Void</B>
            index_set_count: <B>Result</B>.<A HREF="../base/integer_interval_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_minimal_increase"><A HREF="../base/resizable_flatshort.html#f_minimal_increase">minimal_increase</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A> <B>is</B> 5</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Minimal number of additional items</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A><FONT COLOR="red">)</FONT>

    <A NAME="f_occurrences"><A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Number of times </FONT>`c'<FONT COLOR="red"> appears in the string</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/bag_flatshort.html">BAG</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bag_flatshort.html">BAG</A>
            non_negative_occurrences: <B>Result</B> &gt;= 0
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            zero_if_empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0 <B>implies</B> <B>Result</B> = 0
            recurse_if_not_found_at_first_position: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>and then</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1) /= c) <B>implies</B> <B>Result</B> = <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c)
            recurse_if_found_at_first_position: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>and then</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1) = c) <B>implies</B> <B>Result</B> = 1 + <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Comparison</FONT>

    <A NAME="f_deep_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> or attached to isomorphic object structures?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            shallow_implies_deep: <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (some, other) <B>implies</B> <B>Result</B>
            both_or_none_void: (some = <B>Void</B>) <B>implies</B> (<B>Result</B> = (other = <B>Void</B>))
            same_type: (<B>Result</B> <B>and</B> (some /= <B>Void</B>)) <B>implies</B> (other /= <B>Void</B> <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other))
            symmetric: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (other, some)
</A>
    <A NAME="f_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_equal">equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void or attached</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to objects considered equal?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (some = <B>Void</B> <B>and</B> other = <B>Void</B>) <B>or else</B> ((some /= <B>Void</B> <B>and</B> other /= <B>Void</B>) <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (other))
</A>
    <A NAME="f_is_case_insensitive_equal"><A HREF="../base/readable_string_8_flatshort.html#f_is_case_insensitive_equal">is_case_insensitive_equal</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is string made of same character sequence as </FONT>`other'<FONT COLOR="red"> regardless of casing</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (possibly with a different capacity)?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/readable_string_8_flatshort.html#f_is_case_insensitive_equal">is_case_insensitive_equal</A> (<B>Current</B>)
            consistent: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
            valid_result: <A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>.<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (other.<A HREF="../base/readable_string_8_flatshort.html#f_as_lower">as_lower</A>) <B>implies</B> <B>Result</B>
</A>
    <A NAME="f_is_deep_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_is_deep_equal">is_deep_equal</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`Current'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> attached to isomorphic object structures?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            shallow_implies_deep: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
            same_type: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_is_deep_equal">is_deep_equal</A> (<B>Current</B>)
</A>
    <A NAME="f_is_equal"><A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is string made of same character sequence as </FONT>`other'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (possibly with a different capacity)?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
            consistent: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other) <B>implies</B> <B>Result</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            trichotomy: <B>Result</B> = (<B>not</B> (<B>Current</B> &lt; other) <B>and</B> <B>not</B> (other &lt; <B>Current</B>))
</A>
    <A NAME="f_max"><A HREF="../base/comparable_flatshort.html#f_max">max</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> The greater of current object and </FONT>`other'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            current_if_not_smaller: <B>Current</B> &gt;= other <B>implies</B> <B>Result</B> = <B>Current</B>
            other_if_smaller: <B>Current</B> &lt; other <B>implies</B> <B>Result</B> = other
</A>
    <A NAME="f_min"><A HREF="../base/comparable_flatshort.html#f_min">min</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> The smaller of current object and </FONT>`other'
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            current_if_not_greater: <B>Current</B> &lt;= other <B>implies</B> <B>Result</B> = <B>Current</B>
            other_if_greater: <B>Current</B> &gt; other <B>implies</B> <B>Result</B> = other
</A>
    <A NAME="f_same_string"><A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (other: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do </FONT>`Current'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> have same character sequence?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            definition: <B>Result</B> = <A HREF="../base/readable_string_8_flatshort.html#f_string">string</A>.<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (other.<A HREF="../base/readable_string_8_flatshort.html#f_string">string</A>)
</A>
    <A NAME="f_standard_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>; other: <B>like</B> arg #1): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Are </FONT>`some'<FONT COLOR="red"> and </FONT>`other'<FONT COLOR="red"> either both void or attached to</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> field-by-field identical objects of the same type?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Always uses default object comparison criterion.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (some = <B>Void</B> <B>and</B> other = <B>Void</B>) <B>or else</B> ((some /= <B>Void</B> <B>and</B> other /= <B>Void</B>) <B>and then</B> some.<A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other))
</A>
    <A NAME="f_standard_is_equal"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`other'<FONT COLOR="red"> attached to an object of the same type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> as current object, and field-by-field identical to it?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            same_type: <B>Result</B> <B>implies</B> <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
            symmetric: <B>Result</B> <B>implies</B> other.<A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (<B>Current</B>)
</A>
    <A NAME="f_three_way_comparison"><A HREF="../base/comparable_flatshort.html#f_three_way_comparison">three_way_comparison</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> If current object equal to </FONT>`other'<FONT COLOR="red">, 0;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> if smaller, -1; if greater, 1</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            equal_zero: (<B>Result</B> = 0) = <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (other)
            smaller_negative: (<B>Result</B> = -1) = (<B>Current</B> &lt; other)
            greater_positive: (<B>Result</B> = 1) = (<B>Current</B> &gt; other)
</A>
    <A NAME="f_infix "&lt;""><B>infix</B> "&lt;" (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is string lexicographically lower than </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/part_comparable_flatshort.html">PART_COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            asymmetric: <B>Result</B> <B>implies</B> <B>not</B> (other &lt; <B>Current</B>)
</A>
    <A NAME="f_infix "&lt;=""><B>infix</B> "&lt;=" (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current object less than or equal to </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/part_comparable_flatshort.html">PART_COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            definition: <B>Result</B> = ((<B>Current</B> &lt; other) <B>or</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (other))
</A>
    <A NAME="f_infix "&gt;""><B>infix</B> "&gt;" (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current object greater than </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/part_comparable_flatshort.html">PART_COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            definition: <B>Result</B> = (other &lt; <B>Current</B>)
</A>
    <A NAME="f_infix "&gt;=""><B>infix</B> "&gt;=" (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is current object greater than or equal to </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/part_comparable_flatshort.html">PART_COMPARABLE</A>
            other_exists: other /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
            definition: <B>Result</B> = (other &lt;= <B>Current</B>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Status report</FONT>

    <A NAME="f_changeable_comparison_criterion"><A HREF="../base/string_8_flatshort.html#f_changeable_comparison_criterion">changeable_comparison_criterion</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>False</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May </FONT><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A><FONT COLOR="red"> be changed?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Answer: yes by default.)</FONT>

    <A NAME="f_conforms_to"><A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (other: <A HREF="../base/any_flatshort.html">ANY</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does type of current object conform to type</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of </FONT>`other'<FONT COLOR="red"> (as per Eiffel: The Language, chapter 13)?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
</A>
    <A NAME="f_ends_with"><A HREF="../base/readable_string_8_flatshort.html#f_ends_with">ends_with</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does string finish with </FONT>`s'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            argument_not_void: s /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            definition: <B>Result</B> = s.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_extendible"><A HREF="../base/string_8_flatshort.html#f_extendible">extendible</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>True</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May new items be added? (Answer: yes.)</FONT>

    <A NAME="f_full"><A HREF="../base/bounded_flatshort.html#f_full">full</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is structure full?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/bounded_flatshort.html">BOUNDED</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_has"><A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does string include </FONT>`c'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/container_flatshort.html">CONTAINER</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            not_found_in_empty: <B>Result</B> <B>implies</B> <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            false_if_empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0 <B>implies</B> <B>not</B> <B>Result</B>
            true_if_first: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>and then</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1) = c <B>implies</B> <B>Result</B>
            recurse: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>and then</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1) /= c) <B>implies</B> (<B>Result</B> = <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c))
</A>
    <A NAME="f_has_code"><A HREF="../base/readable_string_general_flatshort.html#f_has_code">has_code</A> (c: <B>like</B> <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does string include </FONT>`c'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            false_if_empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0 <B>implies</B> <B>not</B> <B>Result</B>
            true_if_first: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>and then</B> <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (1) = c <B>implies</B> <B>Result</B>
            recurse: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>and then</B> <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (1) /= c) <B>implies</B> (<B>Result</B> = <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_general_flatshort.html#f_has_code">has_code</A> (c))
</A>
    <A NAME="f_has_substring"><A HREF="../base/readable_string_8_flatshort.html#f_has_substring">has_substring</A> (other: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> contain </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            false_if_too_small: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &lt; other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> <B>implies</B> <B>not</B> <B>Result</B>
            true_if_initial: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt;= other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> <B>and then</B> other.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))) <B>implies</B> <B>Result</B>
            recurse: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt;= other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> <B>and then</B> <B>not</B> other.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))) <B>implies</B> (<B>Result</B> = <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_has_substring">has_substring</A> (other))
</A>
    <A NAME="f_is_boolean"><A HREF="../base/readable_string_8_flatshort.html#f_is_boolean">is_boolean</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a BOOLEAN?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_boolean: <B>Result</B> = (<A HREF="../base/readable_string_8_flatshort.html#f_true_constant">true_constant</A>.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>) <B>or</B> <A HREF="../base/readable_string_8_flatshort.html#f_false_constant">false_constant</A>.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>))
</A>
    <A NAME="f_is_double"><A HREF="../base/readable_string_8_flatshort.html#f_is_double">is_double</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a DOUBLE?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_empty"><A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is structure empty?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/finite_flatshort.html">FINITE</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/container_flatshort.html">CONTAINER</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            <B>True</B>
</A>
    <A NAME="f_is_hashable"><A HREF="../base/hashable_flatshort.html#f_is_hashable">is_hashable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May current object be hashed?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (True by default.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/hashable_flatshort.html">HASHABLE</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_immutable"><A HREF="../base/readable_string_general_flatshort.html#f_is_immutable">is_immutable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Can the character sequence of </FONT>`Current'<FONT COLOR="red"> be changed?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_inserted"><A HREF="../base/collection_flatshort.html#f_is_inserted">is_inserted</A> (v: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Has </FONT>`v'<FONT COLOR="red"> been inserted by the most recent insertion?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (By default, the value returned is equivalent to calling </FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT>`has (v)'<FONT COLOR="red">. However, descendants might be able to provide more</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> efficient implementations.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_integer"><A HREF="../base/readable_string_8_flatshort.html#f_is_integer">is_integer</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent an INTEGER_32?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_is_integer_32">is_integer_32</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_integer_16"><A HREF="../base/readable_string_8_flatshort.html#f_is_integer_16">is_integer_16</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent an INTEGER_16?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_integer_32"><A HREF="../base/readable_string_8_flatshort.html#f_is_integer_32">is_integer_32</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent an INTEGER_32?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_is_integer">is_integer</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_integer_64"><A HREF="../base/readable_string_8_flatshort.html#f_is_integer_64">is_integer_64</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent an INTEGER_64?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_integer_8"><A HREF="../base/readable_string_8_flatshort.html#f_is_integer_8">is_integer_8</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent an INTEGER_8?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_natural"><A HREF="../base/readable_string_8_flatshort.html#f_is_natural">is_natural</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a NATURAL_32?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_is_natural_32">is_natural_32</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_natural_16"><A HREF="../base/readable_string_8_flatshort.html#f_is_natural_16">is_natural_16</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a NATURAL_16?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_natural_32"><A HREF="../base/readable_string_8_flatshort.html#f_is_natural_32">is_natural_32</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a NATURAL_32?</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_is_natural">is_natural</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_natural_64"><A HREF="../base/readable_string_8_flatshort.html#f_is_natural_64">is_natural_64</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a NATURAL_64?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_natural_8"><A HREF="../base/readable_string_8_flatshort.html#f_is_natural_8">is_natural_8</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a NATURAL_8?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_number_sequence"><A HREF="../base/readable_string_8_flatshort.html#f_is_number_sequence">is_number_sequence</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a number sequence?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_real"><A HREF="../base/readable_string_8_flatshort.html#f_is_real">is_real</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does </FONT>`Current'<FONT COLOR="red"> represent a REAL?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_is_string_32"><A HREF="../base/readable_string_8_flatshort.html#f_is_string_32">is_string_32</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>False</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`Current'<FONT COLOR="red"> a sequence of CHARACTER_32?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>

    <A NAME="f_is_string_8"><A HREF="../base/readable_string_8_flatshort.html#f_is_string_8">is_string_8</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>True</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`Current'<FONT COLOR="red"> a sequence of CHARACTER_8?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>

    <A NAME="f_is_valid_as_string_8"><A HREF="../base/readable_string_8_flatshort.html#f_is_valid_as_string_8">is_valid_as_string_8</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A> <B>is</B> <B>True</B></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`Current'<FONT COLOR="red"> convertible to a sequence of CHARACTER_8 without information loss?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>

    <A NAME="f_object_comparison"><A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A></A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Must search operations use </FONT><A HREF="../base/any_flatshort.html#f_equal">equal</A><FONT COLOR="red"> rather than </FONT>`='
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> for comparing references? (Default: no, use </FONT>`='<FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A><FONT COLOR="red">)</FONT>

    <A NAME="f_prunable"><A HREF="../base/string_8_flatshort.html#f_prunable">prunable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May items be removed? (Answer: yes.)</FONT>
</A>
    <A NAME="f_resizable"><A HREF="../base/resizable_flatshort.html#f_resizable">resizable</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> May </FONT><A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A><FONT COLOR="red"> be changed? (Answer: yes.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_same_type"><A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other: <A HREF="../base/any_flatshort.html">ANY</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is type of current object identical to type of </FONT>`other'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            definition: <B>Result</B> = (<A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (other) <B>and</B> other.<A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (<B>Current</B>))
</A>
    <A NAME="f_starts_with"><A HREF="../base/readable_string_8_flatshort.html#f_starts_with">starts_with</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Does string begin with </FONT>`s'<FONT COLOR="red">?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            argument_not_void: s /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            definition: <B>Result</B> = s.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_valid_code"><A HREF="../base/readable_string_8_flatshort.html#f_valid_code">valid_code</A> (v: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`v'<FONT COLOR="red"> a valid code for a CHARACTER_32?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            <B>True</B>
</A>
    <A NAME="f_valid_index"><A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Is </FONT>`i'<FONT COLOR="red"> within the bounds of the string?</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/table_flatshort.html">TABLE</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            <B>True</B>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/to_special_flatshort.html">TO_SPECIAL</A>
            <B>True</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            only_if_in_index_set: <B>Result</B> <B>implies</B> ((i &gt;= <A HREF="../base/readable_string_8_flatshort.html#f_index_set">index_set</A>.<A HREF="../base/integer_interval_flatshort.html#f_lower">lower</A>) <B>and</B> (i &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_index_set">index_set</A>.<A HREF="../base/integer_interval_flatshort.html#f_upper">upper</A>))
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Status setting</FONT>

    <A NAME="f_compare_objects"><A HREF="../base/container_flatshort.html#f_compare_objects">compare_objects</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that future search operations will use </FONT><A HREF="../base/any_flatshort.html#f_equal">equal</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> rather than </FONT>`='<FONT COLOR="red"> for comparing references.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            changeable_comparison_criterion: <A HREF="../base/string_8_flatshort.html#f_changeable_comparison_criterion">changeable_comparison_criterion</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>
    <A NAME="f_compare_references"><A HREF="../base/container_flatshort.html#f_compare_references">compare_references</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that future search operations will use </FONT>`='
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> rather than </FONT><A HREF="../base/any_flatshort.html#f_equal">equal</A><FONT COLOR="red"> for comparing references.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            changeable_comparison_criterion: <A HREF="../base/string_8_flatshort.html#f_changeable_comparison_criterion">changeable_comparison_criterion</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/container_flatshort.html">CONTAINER</A>
            reference_comparison: <B>not</B> <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Element change</FONT>

    <A NAME="f_append"><A HREF="../base/string_8_flatshort.html#f_append">append</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append a copy of </FONT>`s'<FONT COLOR="red"> at end.</FONT>
        <B>require</B>
            argument_not_void: s /= <B>Void</B>
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + <B>old</B> s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            appended: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A> + <B>old</B> s.<A HREF="../base/any_flatshort.html#f_twin">twin</A>)
</A>
    <A NAME="f_append_boolean"><A HREF="../base/string_8_flatshort.html#f_append_boolean">append_boolean</A> (b: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`b'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_character"><A HREF="../base/string_8_flatshort.html#f_append_character">append_character</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append </FONT>`c'<FONT COLOR="red"> at end.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/string_8_flatshort.html#f_extend">extend</A><FONT COLOR="red">.</FONT>
        <B>ensure then</B>
            item_inserted: <A HREF="../base/string_8_flatshort.html#f_item">item</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) = c
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
            stable_before: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 1).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>)
</A>
    <A NAME="f_append_code"><A HREF="../base/string_general_flatshort.html#f_append_code">append_code</A> (c: <B>like</B> <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append </FONT>`c'<FONT COLOR="red"> at end.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            valid_code: <A HREF="../base/readable_string_8_flatshort.html#f_valid_code">valid_code</A> (c)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            item_inserted: <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) = c
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
            stable_before: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 1).<A HREF="../base/comparable_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>)
</A>
    <A NAME="f_append_double"><A HREF="../base/string_8_flatshort.html#f_append_double">append_double</A> (d: <A HREF="../base/real_64_flatshort.html">REAL_64</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`d'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_integer"><A HREF="../base/string_8_flatshort.html#f_append_integer">append_integer</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_integer_16"><A HREF="../base/string_8_flatshort.html#f_append_integer_16">append_integer_16</A> (i: <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_integer_64"><A HREF="../base/string_8_flatshort.html#f_append_integer_64">append_integer_64</A> (i: <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_integer_8"><A HREF="../base/string_8_flatshort.html#f_append_integer_8">append_integer_8</A> (i: <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_natural_16"><A HREF="../base/string_8_flatshort.html#f_append_natural_16">append_natural_16</A> (i: <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_natural_32"><A HREF="../base/string_8_flatshort.html#f_append_natural_32">append_natural_32</A> (i: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_natural_64"><A HREF="../base/string_8_flatshort.html#f_append_natural_64">append_natural_64</A> (i: <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_natural_8"><A HREF="../base/string_8_flatshort.html#f_append_natural_8">append_natural_8</A> (i: <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`i'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_real"><A HREF="../base/string_8_flatshort.html#f_append_real">append_real</A> (r: <A HREF="../base/real_32_flatshort.html">REAL_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append the string representation of </FONT>`r'<FONT COLOR="red"> at end.</FONT>
</A>
    <A NAME="f_append_string"><A HREF="../base/string_8_flatshort.html#f_append_string">append_string</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append a copy of </FONT>`s'<FONT COLOR="red">, if not void, at end.</FONT>
        <B>ensure</B>
            appended: s /= <B>Void</B> <B>implies</B> (<A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A> + <B>old</B> s.<A HREF="../base/any_flatshort.html#f_twin">twin</A>))
</A>
    <A NAME="f_append_string_general"><A HREF="../base/string_8_flatshort.html#f_append_string_general">append_string_general</A> (s: <A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append a copy of </FONT>`s'<FONT COLOR="red"> at end.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            argument_not_void: s /= <B>Void</B>
            compatible_strings: <A HREF="../base/readable_string_8_flatshort.html#f_is_string_8">is_string_8</A> <B>implies</B> s.<A HREF="../base/readable_string_general_flatshort.html#f_is_valid_as_string_8">is_valid_as_string_8</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + <B>old</B> s.<A HREF="../base/readable_string_general_flatshort.html#f_count">count</A>
            appended: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A>.<A HREF="../base/readable_string_32_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A>.<A HREF="../base/any_flatshort.html#f_twin">twin</A> + <B>old</B> s.<A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A>.<A HREF="../base/any_flatshort.html#f_twin">twin</A>)
</A>
    <A NAME="f_extend"><A HREF="../base/string_8_flatshort.html#f_extend">extend</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append </FONT>`c'<FONT COLOR="red"> at end.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/string_8_flatshort.html#f_append_character">append_character</A><FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            extendible: <A HREF="../base/string_8_flatshort.html#f_extendible">extendible</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            item_inserted: <A HREF="../base/collection_flatshort.html#f_is_inserted">is_inserted</A> (c)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bag_flatshort.html">BAG</A>
            one_more_occurrence: <A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c) = <B>old</B> (<A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c)) + 1
        <B>ensure then</B>
            item_inserted: <A HREF="../base/string_8_flatshort.html#f_item">item</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) = c
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
            stable_before: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 1).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>)
</A>
    <A NAME="f_fill"><A HREF="../base/collection_flatshort.html#f_fill">fill</A> (other: <A HREF="../base/container_flatshort.html">CONTAINER</A> [<A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>])
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Fill with as many items of </FONT>`other'<FONT COLOR="red"> as possible.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> The representations of </FONT>`other'<FONT COLOR="red"> and current structure</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> need not be the same.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            other_not_void: other /= <B>Void</B>
            extendible: <A HREF="../base/string_8_flatshort.html#f_extendible">extendible</A>
</A>
    <A NAME="f_fill_blank"><A HREF="../base/string_8_flatshort.html#f_fill_blank">fill_blank</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Fill with </FONT><A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A><FONT COLOR="red"> blank characters.</FONT>
        <B>ensure</B>
            filled: <A HREF="../base/bounded_flatshort.html#f_full">full</A>
            same_size: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>) <B>and</B> (<A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>)
</A>
    <A NAME="f_fill_character"><A HREF="../base/readable_string_8_flatshort.html#f_fill_character">fill_character</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Fill with </FONT><A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A><FONT COLOR="red"> characters all equal to </FONT>`c'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            filled: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>
            same_size: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>
</A>
    <A NAME="f_fill_with"><A HREF="../base/string_8_flatshort.html#f_fill_with">fill_with</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace every character with </FONT>`c'<FONT COLOR="red">.</FONT>
        <B>ensure</B>
            same_count: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) <B>and</B> (<A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>)
            filled: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c) = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_insert_character"><A HREF="../base/string_8_flatshort.html#f_insert_character">insert_character</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`c'<FONT COLOR="red"> at index </FONT>`i'<FONT COLOR="red">, shifting characters between ranks</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT>`i'<FONT COLOR="red"> and </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red"> rightwards.</FONT>
        <B>require</B>
            valid_insertion_index: 1 &lt;= i <B>and</B> i &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
        <B>ensure</B>
            one_more_character: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
            inserted: <A HREF="../base/string_8_flatshort.html#f_item">item</A> (i) = c
            stable_before_i: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1))
            stable_after_i: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_insert_string"><A HREF="../base/string_8_flatshort.html#f_insert_string">insert_string</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>; i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Insert </FONT>`s'<FONT COLOR="red"> at index </FONT>`i'<FONT COLOR="red">, shifting characters between ranks</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT>`i'<FONT COLOR="red"> and </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red"> rightwards.</FONT>
        <B>require</B>
            string_exists: s /= <B>Void</B>
            valid_insertion_index: 1 &lt;= i <B>and</B> i &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
        <B>ensure</B>
            inserted: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> (<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1) + <B>old</B> (s.<A HREF="../base/any_flatshort.html#f_twin">twin</A>) + <B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)))
</A>
    <A NAME="f_keep_head"><A HREF="../base/string_8_flatshort.html#f_keep_head">keep_head</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all characters except for the first </FONT>`n'<FONT COLOR="red">;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> do nothing if </FONT>`n'<FONT COLOR="red"> &gt;= </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red">.</FONT>
        <B>require</B>
            non_negative_argument: n &gt;= 0
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = n.<A HREF="../base/comparable_flatshort.html#f_min">min</A> (<B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)
            kept: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, n.<A HREF="../base/comparable_flatshort.html#f_min">min</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)))
</A>
    <A NAME="f_keep_tail"><A HREF="../base/string_8_flatshort.html#f_keep_tail">keep_tail</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all characters except for the last </FONT>`n'<FONT COLOR="red">;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> do nothing if </FONT>`n'<FONT COLOR="red"> &gt;= </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red">.</FONT>
        <B>require</B>
            non_negative_argument: n &gt;= 0
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = n.<A HREF="../base/comparable_flatshort.html#f_min">min</A> (<B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)
            kept: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - n.<A HREF="../base/comparable_flatshort.html#f_min">min</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_left_adjust"><A HREF="../base/string_8_flatshort.html#f_left_adjust">left_adjust</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove leading whitespace.</FONT>
        <B>ensure</B>
            valid_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &lt;= <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            new_count: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> <B>implies</B> <B>not</B> <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1).<A HREF="../base/character_8_ref_flatshort.html#f_is_space">is_space</A>
            kept: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> ((<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>).<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (<B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1, <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_precede"><A HREF="../base/string_8_flatshort.html#f_precede">precede</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add </FONT>`c'<FONT COLOR="red"> at front.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/string_8_flatshort.html#f_prepend_character">prepend_character</A><FONT COLOR="red">.</FONT>
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
</A>
    <A NAME="f_prepend"><A HREF="../base/string_8_flatshort.html#f_prepend">prepend</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Prepend a copy of </FONT>`s'<FONT COLOR="red"> at front.</FONT>
        <B>require</B>
            argument_not_void: s /= <B>Void</B>
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)
            inserted: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_string">string</A>.<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> (s.<A HREF="../base/any_flatshort.html#f_twin">twin</A>.<A HREF="../base/readable_string_general_flatshort.html#f_as_string_8">as_string_8</A>) + <B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_prepend_boolean"><A HREF="../base/string_8_flatshort.html#f_prepend_boolean">prepend_boolean</A> (b: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Prepend the string representation of </FONT>`b'<FONT COLOR="red"> at front.</FONT>
</A>
    <A NAME="f_prepend_character"><A HREF="../base/string_8_flatshort.html#f_prepend_character">prepend_character</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Add </FONT>`c'<FONT COLOR="red"> at front.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/string_8_flatshort.html#f_precede">precede</A><FONT COLOR="red">.</FONT>
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1
</A>
    <A NAME="f_prepend_double"><A HREF="../base/string_8_flatshort.html#f_prepend_double">prepend_double</A> (d: <A HREF="../base/real_64_flatshort.html">REAL_64</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Prepend the string representation of </FONT>`d'<FONT COLOR="red"> at front.</FONT>
</A>
    <A NAME="f_prepend_integer"><A HREF="../base/string_8_flatshort.html#f_prepend_integer">prepend_integer</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Prepend the string representation of </FONT>`i'<FONT COLOR="red"> at front.</FONT>
</A>
    <A NAME="f_prepend_real"><A HREF="../base/string_8_flatshort.html#f_prepend_real">prepend_real</A> (r: <A HREF="../base/real_32_flatshort.html">REAL_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Prepend the string representation of </FONT>`r'<FONT COLOR="red"> at front.</FONT>
</A>
    <A NAME="f_prepend_string"><A HREF="../base/string_8_flatshort.html#f_prepend_string">prepend_string</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Prepend a copy of </FONT>`s'<FONT COLOR="red">, if not void, at front.</FONT>
</A>
    <A NAME="f_put"><A HREF="../base/string_8_flatshort.html#f_put">put</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace character at position </FONT>`i'<FONT COLOR="red"> by </FONT>`c'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/table_flatshort.html">TABLE</A>
            valid_key: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/to_special_flatshort.html">TO_SPECIAL</A>
            valid_index: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/to_special_flatshort.html">TO_SPECIAL</A>
            inserted: <A HREF="../base/string_8_flatshort.html#f_item">item</A> (i) = c
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
            insertion_done: <A HREF="../base/string_8_flatshort.html#f_item">item</A> (i) = c
        <B>ensure then</B>
            stable_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            stable_before_i: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1))
            stable_after_i: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_put_code"><A HREF="../base/string_8_flatshort.html#f_put_code">put_code</A> (v: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>; i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace character at position </FONT>`i'<FONT COLOR="red"> by character of code </FONT>`v'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            valid_code: <A HREF="../base/readable_string_8_flatshort.html#f_valid_code">valid_code</A> (v)
            valid_index: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            inserted: <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (i) = v
            stable_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            stable_before_i: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1).<A HREF="../base/comparable_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1))
            stable_after_i: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/comparable_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_replace_blank"><A HREF="../base/string_8_flatshort.html#f_replace_blank">replace_blank</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace all current characters with blanks.</FONT>
        <B>ensure</B>
            same_size: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) <B>and</B> (<A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>)
            all_blank: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (' ') = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_replace_substring"><A HREF="../base/string_8_flatshort.html#f_replace_substring">replace_substring</A> (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>; start_index, end_index: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace characters from </FONT>`start_index'<FONT COLOR="red"> to </FONT>`end_index'<FONT COLOR="red"> with </FONT>`s'<FONT COLOR="red">.</FONT>
        <B>require</B>
            string_not_void: s /= <B>Void</B>
            valid_start_index: 1 &lt;= start_index
            valid_end_index: end_index &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            meaningfull_interval: start_index &lt;= end_index + 1
        <B>ensure</B>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + <B>old</B> s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - end_index + start_index - 1
            replaced: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> (<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, start_index - 1) + s + <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (end_index + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))))
</A>
    <A NAME="f_replace_substring_all"><A HREF="../base/string_8_flatshort.html#f_replace_substring_all">replace_substring_all</A> (original, new: <B>like</B> <B>Current</B>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Replace every occurrence of </FONT>`original'<FONT COLOR="red"> with </FONT>`new'<FONT COLOR="red">.</FONT>
        <B>require</B>
            original_exists: original /= <B>Void</B>
            new_exists: new /= <B>Void</B>
            original_not_empty: <B>not</B> original.<A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_right_adjust"><A HREF="../base/string_8_flatshort.html#f_right_adjust">right_adjust</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove trailing whitespace.</FONT>
        <B>ensure</B>
            valid_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &lt;= <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            new_count: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> /= 0) <B>implies</B> ((<A HREF="../base/string_8_flatshort.html#f_item">item</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) /= ' ') <B>and</B> (<A HREF="../base/string_8_flatshort.html#f_item">item</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) /= '%T') <B>and</B> (<A HREF="../base/string_8_flatshort.html#f_item">item</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) /= '%R') <B>and</B> (<A HREF="../base/string_8_flatshort.html#f_item">item</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) /= '%N'))
            kept: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> ((<B>old</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>).<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_set"><A HREF="../base/string_8_flatshort.html#f_set">set</A> (t: <B>like</B> <B>Current</B>; n1, n2: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Set current string to substring of </FONT>`t'<FONT COLOR="red"> from indices </FONT>`n1'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to </FONT>`n2'<FONT COLOR="red">, or to empty string if no such substring.</FONT>
        <B>require</B>
            argument_not_void: t /= <B>Void</B>
        <B>ensure</B>
            is_substring: <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (t.<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (n1, n2))
</A>
    <A NAME="f_share"><A HREF="../base/string_8_flatshort.html#f_share">share</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Make current string share the text of </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Subsequent changes to the characters of current string</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> will also affect </FONT>`other'<FONT COLOR="red">, and conversely.</FONT>
        <B>require</B>
            argument_not_void: other /= <B>Void</B>
        <B>ensure</B>
            shared_count: other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            shared_area: other.<A HREF="../base/string_8_flatshort.html#f_area">area</A> = <A HREF="../base/string_8_flatshort.html#f_area">area</A>
</A>
    <A NAME="f_subcopy"><A HREF="../base/string_8_flatshort.html#f_subcopy">subcopy</A> (other: <B>like</B> <B>Current</B>; start_pos, end_pos, index_pos: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy characters of </FONT>`other'<FONT COLOR="red"> within bounds </FONT>`start_pos'<FONT COLOR="red"> and</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT>`end_pos'<FONT COLOR="red"> to current string starting at index </FONT>`index_pos'<FONT COLOR="red">.</FONT>
        <B>require</B>
            other_not_void: other /= <B>Void</B>
            valid_start_pos: other.<A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (start_pos)
            valid_end_pos: other.<A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (end_pos)
            valid_bounds: (start_pos &lt;= end_pos) <B>or</B> (start_pos = end_pos + 1)
            valid_index_pos: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (index_pos)
            enough_space: (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - index_pos) &gt;= (end_pos - start_pos)
        <B>ensure</B>
            same_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            copied: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> (<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, index_pos - 1) + <B>old</B> other.<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_pos, end_pos) + <B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (index_pos + (end_pos - start_pos + 1), <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)))
</A>
    <A NAME="f_infix "+""><B>infix</B> "+" (s: <A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>): <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Append a copy of 's' at the end of a copy of Current,</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Then return the Result.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            argument_not_void: s /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            result_exists: <B>Result</B> /= <B>Void</B>
            new_count: <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            initial: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
            final: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_substring">substring</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> + s.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (s)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Removal</FONT>

    <A NAME="f_clear_all"><A HREF="../base/string_8_flatshort.html#f_clear_all">clear_all</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Reset all characters.</FONT>
        <B>ensure</B>
            is_empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0
            same_capacity: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>
</A>
    <A NAME="f_prune"><A HREF="../base/string_8_flatshort.html#f_prune">prune</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove first occurrence of </FONT>`c'<FONT COLOR="red">, if any.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            prunable: <A HREF="../base/string_8_flatshort.html#f_prunable">prunable</A>
        <B>require else</B>
            <B>True</B>
</A>
    <A NAME="f_prune_all"><A HREF="../base/string_8_flatshort.html#f_prune_all">prune_all</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all occurrences of </FONT>`c'<FONT COLOR="red">.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            prunable: <A HREF="../base/string_8_flatshort.html#f_prunable">prunable</A>
        <B>require else</B>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            no_more_occurrences: <B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_has">has</A> (c)
        <B>ensure then</B>
            changed_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = (<B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) - (<B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_occurrences">occurrences</A> (c))
</A>
    <A NAME="f_prune_all_leading"><A HREF="../base/string_8_flatshort.html#f_prune_all_leading">prune_all_leading</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all leading occurrences of </FONT>`c'<FONT COLOR="red">.</FONT>
</A>
    <A NAME="f_prune_all_trailing"><A HREF="../base/string_8_flatshort.html#f_prune_all_trailing">prune_all_trailing</A> (c: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all trailing occurrences of </FONT>`c'<FONT COLOR="red">.</FONT>
</A>
    <A NAME="f_remove"><A HREF="../base/string_8_flatshort.html#f_remove">remove</A> (i: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove </FONT>`i'<FONT COLOR="red">-th character.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            valid_index: <A HREF="../base/readable_string_8_flatshort.html#f_valid_index">valid_index</A> (i)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            new_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - 1
            removed: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A>.<A HREF="../base/readable_string_32_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, i - 1).<A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A> + <B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (i + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A>)
</A>
    <A NAME="f_remove_head"><A HREF="../base/string_8_flatshort.html#f_remove_head">remove_head</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove first </FONT>`n'<FONT COLOR="red"> characters;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> if </FONT>`n'<FONT COLOR="red"> &gt; </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red">, remove all.</FONT>
        <B>require</B>
            n_non_negative: n &gt;= 0
        <B>ensure</B>
            removed: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (n.<A HREF="../base/comparable_flatshort.html#f_min">min</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>) + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_remove_substring"><A HREF="../base/string_8_flatshort.html#f_remove_substring">remove_substring</A> (start_index, end_index: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all characters from </FONT>`start_index'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to </FONT>`end_index'<FONT COLOR="red"> inclusive.</FONT>
        <B>require</B>
            valid_start_index: 1 &lt;= start_index
            valid_end_index: end_index &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            meaningful_interval: start_index &lt;= end_index + 1
        <B>ensure</B>
            removed: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, start_index - 1) + <B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (end_index + 1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>))
</A>
    <A NAME="f_remove_tail"><A HREF="../base/string_8_flatshort.html#f_remove_tail">remove_tail</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove last </FONT>`n'<FONT COLOR="red"> characters;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> if </FONT>`n'<FONT COLOR="red"> &gt; </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red">, remove all.</FONT>
        <B>require</B>
            n_non_negative: n &gt;= 0
        <B>ensure</B>
            removed: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (1, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> - n.<A HREF="../base/comparable_flatshort.html#f_min">min</A> (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>)))
</A>
    <A NAME="f_wipe_out"><A HREF="../base/string_8_flatshort.html#f_wipe_out">wipe_out</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Remove all characters.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            prunable: <A HREF="../base/string_8_flatshort.html#f_prunable">prunable</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/collection_flatshort.html">COLLECTION</A>
            wiped_out: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
        <B>ensure then</B>
            is_empty: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0
            empty_capacity: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> = 0
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Resizing</FONT>

    <A NAME="f_adapt_size"><A HREF="../base/string_8_flatshort.html#f_adapt_size">adapt_size</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Adapt the size to accommodate </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red"> characters.</FONT>
</A>
    <A NAME="f_automatic_grow"><A HREF="../base/resizable_flatshort.html#f_automatic_grow">automatic_grow</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Change the capacity to accommodate at least</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT><A HREF="../base/resizable_flatshort.html#f_growth_percentage">Growth_percentage</A><FONT COLOR="red"> more items.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A>
            increased_capacity: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> + <B>old</B> <A HREF="../base/resizable_flatshort.html#f_additional_space">additional_space</A>
</A>
    <A NAME="f_grow"><A HREF="../base/string_8_flatshort.html#f_grow">grow</A> (newsize: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Ensure that the capacity is at least </FONT>`newsize'<FONT COLOR="red">.</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A>
            new_capacity: <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A> &gt;= newsize
</A>
    <A NAME="f_resize"><A HREF="../base/string_8_flatshort.html#f_resize">resize</A> (newsize: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Rearrange string so that it can accommodate</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> at least </FONT>`newsize'<FONT COLOR="red"> characters.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Do not lose any previously entered character.</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
            new_size_non_negative: newsize &gt;= 0
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Transformation</FONT>

    <A NAME="f_correct_mismatch"><A HREF="../base/string_8_flatshort.html#f_correct_mismatch">correct_mismatch</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Attempt to correct object mismatch during retrieve using </FONT><A HREF="../base/mismatch_corrector_flatshort.html#f_mismatch_information">Mismatch_information</A><FONT COLOR="red">.</FONT>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Conversion</FONT>

    <A NAME="f_as_lower"><A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>: <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object with all letters in lower case.</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            length: <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            anchor: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_item">item</A> (1) = <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1).<A HREF="../base/character_8_ref_flatshort.html#f_as_lower">as_lower</A>
            recurse: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 1 <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_as_lower">as_lower</A>)
</A>
    <A NAME="f_as_string_32"><A HREF="../base/readable_string_general_flatshort.html#f_as_string_32">as_string_32</A>: <A HREF="../base/string_32_flatshort.html">STRING_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Convert </FONT>`Current'<FONT COLOR="red"> as a STRING_32.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            as_string_32_not_void: <B>Result</B> /= <B>Void</B>
            identity: (<A HREF="../base/readable_string_8_flatshort.html#f_is_string_32">is_string_32</A> <B>and</B> <B>Result</B> = <B>Current</B>) <B>or</B> (<B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_string_32">is_string_32</A> <B>and</B> <B>Result</B> /= <B>Current</B>)
</A>
    <A NAME="f_as_string_8"><A HREF="../base/readable_string_general_flatshort.html#f_as_string_8">as_string_8</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Convert </FONT>`Current'<FONT COLOR="red"> as a STRING_8. If a code of </FONT>`Current'<FONT COLOR="red"> is</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> node a valid code for a STRING_8 it is replaced with the null</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> character.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            as_string_8_not_void: <B>Result</B> /= <B>Void</B>
            identity: (<A HREF="../base/readable_string_8_flatshort.html#f_is_string_8">is_string_8</A> <B>and</B> <B>Result</B> = <B>Current</B>) <B>or</B> (<B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_string_8">is_string_8</A> <B>and</B> <B>Result</B> /= <B>Current</B>)
</A>
    <A NAME="f_as_upper"><A HREF="../base/string_8_flatshort.html#f_as_upper">as_upper</A>: <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object with all letters in upper case</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            length: <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
            anchor: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 0 <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_item">item</A> (1) = <A HREF="../base/string_8_flatshort.html#f_item">item</A> (1).<A HREF="../base/character_8_ref_flatshort.html#f_as_upper">as_upper</A>
            recurse: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt; 1 <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (2, <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>).<A HREF="../base/readable_string_8_flatshort.html#f_as_upper">as_upper</A>)
</A>
    <A NAME="f_center_justify"><A HREF="../base/string_8_flatshort.html#f_center_justify">center_justify</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Center justify Current using </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red"> as width.</FONT>
</A>
    <A NAME="f_character_justify"><A HREF="../base/string_8_flatshort.html#f_character_justify">character_justify</A> (pivot: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>; position: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Justify a string based on a </FONT>`pivot'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> and the </FONT>`position'<FONT COLOR="red"> it needs to be in</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> the final string.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> This will grow the string if necessary</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> to get the pivot in the correct place.</FONT>
        <B>require</B>
            valid_position: position &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>
            positive_position: position &gt;= 1
            pivot_not_space: pivot /= ' '
            not_empty: <B>not</B> <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A>
</A>
    <A NAME="f_left_justify"><A HREF="../base/string_8_flatshort.html#f_left_justify">left_justify</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Left justify Current using </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red"> as witdth.</FONT>
</A>
    <A NAME="f_linear_representation"><A HREF="../base/string_8_flatshort.html#f_linear_representation">linear_representation</A>: <A HREF="../base/linear_flatshort.html">LINEAR</A> [<A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Representation as a linear structure</FONT>
</A>
    <A NAME="f_mirror"><A HREF="../base/string_8_flatshort.html#f_mirror">mirror</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Reverse the order of characters.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> "Hello world" -&gt; "dlrow olleH".</FONT>
        <B>ensure</B>
            same_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_mirrored"><A HREF="../base/string_8_flatshort.html#f_mirrored">mirrored</A>: <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Mirror image of string;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Result for "Hello world" is "dlrow olleH".</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            same_count: <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_right_justify"><A HREF="../base/string_8_flatshort.html#f_right_justify">right_justify</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Right justify Current using </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red"> as width.</FONT>
        <B>ensure</B>
            same_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <B>old</B> <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_split"><A HREF="../base/readable_string_8_flatshort.html#f_split">split</A> (a_separator: <A HREF="../base/character_8_flatshort.html">CHARACTER_8</A>): <A HREF="../base/list_flatshort.html">LIST</A> [<A HREF="../base/string_8_flatshort.html">STRING_8</A>]
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Split on </FONT>`a_separator'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_to_boolean"><A HREF="../base/readable_string_8_flatshort.html#f_to_boolean">to_boolean</A>: <A HREF="../base/boolean_flatshort.html">BOOLEAN</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Boolean value;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> "True" yields </FONT>`True'<FONT COLOR="red">, "False" yields </FONT>`False'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (case-insensitive)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_boolean: <A HREF="../base/readable_string_8_flatshort.html#f_is_boolean">is_boolean</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            to_boolean: (<B>Result</B> = <A HREF="../base/readable_string_8_flatshort.html#f_true_constant">true_constant</A>.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>)) <B>or</B> (<B>not</B> <B>Result</B> = <A HREF="../base/readable_string_8_flatshort.html#f_false_constant">false_constant</A>.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>))
</A>
    <A NAME="f_to_c"><B>frozen</B> <A HREF="../base/string_8_flatshort.html#f_to_c">to_c</A>: <A HREF="../base/any_flatshort.html">ANY</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> A reference to a C form of current string.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Useful only for interfacing with C software.</FONT>
        <B>require</B>
            not_is_dotnet: <B>not</B> {<A HREF="../base/platform_flatshort.html">PLATFORM</A>}.<A HREF="../base/platform_flatshort.html#f_is_dotnet">is_dotnet</A>
</A>
    <A NAME="f_to_cil"><B>frozen</B> <A HREF="../base/readable_string_general_flatshort.html#f_to_cil">to_cil</A>: <A HREF="../base/system_string_flatshort.html">SYSTEM_STRING</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Create an instance of SYSTEM_STRING using characters</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of Current between indices </FONT>`1'<FONT COLOR="red"> and </FONT><A HREF="../base/readable_string_8_flatshort.html#f_count">count</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            is_dotnet: {<A HREF="../base/platform_flatshort.html">PLATFORM</A>}.<A HREF="../base/platform_flatshort.html#f_is_dotnet">is_dotnet</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            to_cil_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_to_double"><A HREF="../base/readable_string_8_flatshort.html#f_to_double">to_double</A>: <A HREF="../base/real_64_flatshort.html">REAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> "Double" value;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> for example, when applied to "123.0", will yield 123.0 (double)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            represents_a_double: <A HREF="../base/readable_string_8_flatshort.html#f_is_double">is_double</A>
</A>
    <A NAME="f_to_integer"><A HREF="../base/readable_string_8_flatshort.html#f_to_integer">to_integer</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 32-bit integer value</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_to_integer_32">to_integer_32</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_integer: <A HREF="../base/readable_string_8_flatshort.html#f_is_integer_32">is_integer_32</A>
</A>
    <A NAME="f_to_integer_16"><A HREF="../base/readable_string_8_flatshort.html#f_to_integer_16">to_integer_16</A>: <A HREF="../base/integer_16_flatshort.html">INTEGER_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 16-bit integer value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_integer_16: <A HREF="../base/readable_string_8_flatshort.html#f_is_integer_16">is_integer_16</A>
</A>
    <A NAME="f_to_integer_32"><A HREF="../base/readable_string_8_flatshort.html#f_to_integer_32">to_integer_32</A>: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 32-bit integer value</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_to_integer">to_integer</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_integer: <A HREF="../base/readable_string_8_flatshort.html#f_is_integer_32">is_integer_32</A>
</A>
    <A NAME="f_to_integer_64"><A HREF="../base/readable_string_8_flatshort.html#f_to_integer_64">to_integer_64</A>: <A HREF="../base/integer_64_flatshort.html">INTEGER_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 64-bit integer value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_integer_64: <A HREF="../base/readable_string_8_flatshort.html#f_is_integer_64">is_integer_64</A>
</A>
    <A NAME="f_to_integer_8"><A HREF="../base/readable_string_8_flatshort.html#f_to_integer_8">to_integer_8</A>: <A HREF="../base/integer_8_flatshort.html">INTEGER_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 8-bit integer value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_integer_8: <A HREF="../base/readable_string_8_flatshort.html#f_is_integer_8">is_integer_8</A>
</A>
    <A NAME="f_to_lower"><A HREF="../base/string_8_flatshort.html#f_to_lower">to_lower</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Convert to lower case.</FONT>
        <B>ensure</B>
            length_end_content: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_as_lower">as_lower</A>)
</A>
    <A NAME="f_to_natural"><A HREF="../base/readable_string_8_flatshort.html#f_to_natural">to_natural</A>: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 32-bit natural value</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_to_natural_32">to_natural_32</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_natural: <A HREF="../base/readable_string_8_flatshort.html#f_is_natural_32">is_natural_32</A>
</A>
    <A NAME="f_to_natural_16"><A HREF="../base/readable_string_8_flatshort.html#f_to_natural_16">to_natural_16</A>: <A HREF="../base/natural_16_flatshort.html">NATURAL_16</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 16-bit natural value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_natural_16: <A HREF="../base/readable_string_8_flatshort.html#f_is_natural_16">is_natural_16</A>
</A>
    <A NAME="f_to_natural_32"><A HREF="../base/readable_string_8_flatshort.html#f_to_natural_32">to_natural_32</A>: <A HREF="../base/natural_32_flatshort.html">NATURAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 32-bit natural value</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_8_flatshort.html#f_to_natural">to_natural</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_natural: <A HREF="../base/readable_string_8_flatshort.html#f_is_natural_32">is_natural_32</A>
</A>
    <A NAME="f_to_natural_64"><A HREF="../base/readable_string_8_flatshort.html#f_to_natural_64">to_natural_64</A>: <A HREF="../base/natural_64_flatshort.html">NATURAL_64</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 64-bit natural value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_natural_64: <A HREF="../base/readable_string_8_flatshort.html#f_is_natural_64">is_natural_64</A>
</A>
    <A NAME="f_to_natural_8"><A HREF="../base/readable_string_8_flatshort.html#f_to_natural_8">to_natural_8</A>: <A HREF="../base/natural_8_flatshort.html">NATURAL_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> 8-bit natural value</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            is_natural_8: <A HREF="../base/readable_string_8_flatshort.html#f_is_natural_8">is_natural_8</A>
</A>
    <A NAME="f_to_real"><A HREF="../base/readable_string_8_flatshort.html#f_to_real">to_real</A>: <A HREF="../base/real_32_flatshort.html">REAL_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Real value;</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> for example, when applied to "123.0", will yield 123.0</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            represents_a_real: <A HREF="../base/readable_string_8_flatshort.html#f_is_real">is_real</A>
</A>
    <A NAME="f_to_string_32"><A HREF="../base/readable_string_general_flatshort.html#f_to_string_32">to_string_32</A>: <A HREF="../base/string_32_flatshort.html">STRING_32</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Convert </FONT>`Current'<FONT COLOR="red"> as a STRING_32.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Was declared in </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red"> as synonym of </FONT><A HREF="../base/readable_string_general_flatshort.html#f_as_string_32">as_string_32</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            as_string_32_not_void: <B>Result</B> /= <B>Void</B>
            identity: (<A HREF="../base/readable_string_8_flatshort.html#f_is_string_32">is_string_32</A> <B>and</B> <B>Result</B> = <B>Current</B>) <B>or</B> (<B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_string_32">is_string_32</A> <B>and</B> <B>Result</B> /= <B>Current</B>)
</A>
    <A NAME="f_to_string_8"><A HREF="../base/readable_string_general_flatshort.html#f_to_string_8">to_string_8</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Convert </FONT>`Current'<FONT COLOR="red"> as a STRING_8.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            is_valid_as_string_8: <A HREF="../base/readable_string_8_flatshort.html#f_is_valid_as_string_8">is_valid_as_string_8</A>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            as_string_8_not_void: <B>Result</B> /= <B>Void</B>
            identity: (<A HREF="../base/readable_string_8_flatshort.html#f_is_string_8">is_string_8</A> <B>and</B> <B>Result</B> = <B>Current</B>) <B>or</B> (<B>not</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_string_8">is_string_8</A> <B>and</B> <B>Result</B> /= <B>Current</B>)
</A>
    <A NAME="f_to_upper"><A HREF="../base/string_8_flatshort.html#f_to_upper">to_upper</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Convert to upper case.</FONT>
        <B>ensure</B>
            length_end_content: <A HREF="../base/readable_string_general_flatshort.html#f_elks_checking">elks_checking</A> <B>implies</B> <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (<B>old</B> <A HREF="../base/string_8_flatshort.html#f_as_upper">as_upper</A>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Duplication</FONT>

    <A NAME="f_copy"><A HREF="../base/readable_string_8_flatshort.html#f_copy">copy</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Reinitialize by copying the characters of </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (This is also used by </FONT><A HREF="../base/any_flatshort.html#f_twin">twin</A><FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
            type_identity: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            is_equal: <A HREF="../base/readable_string_8_flatshort.html#f_is_equal">is_equal</A> (other)
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            new_result_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = other.<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A>
</A>
    <A NAME="f_deep_copy"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_copy">deep_copy</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Effect equivalent to that of:</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red">		</FONT><A HREF="../base/readable_string_8_flatshort.html#f_copy">copy</A><FONT COLOR="red"> (</FONT>`other'<FONT COLOR="red"> . </FONT><A HREF="../base/any_flatshort.html#f_deep_twin">deep_twin</A><FONT COLOR="red">)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            deep_equal: <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (<B>Current</B>, other)
</A>
    <A NAME="f_deep_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_deep_twin">deep_twin</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object structure recursively duplicated from Current.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            deep_twin_not_void: <B>Result</B> /= <B>Void</B>
            deep_equal: <A HREF="../base/any_flatshort.html#f_deep_equal">deep_equal</A> (<B>Current</B>, <B>Result</B>)
</A>
    <A NAME="f_multiply"><A HREF="../base/string_8_flatshort.html#f_multiply">multiply</A> (n: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Duplicate a string within itself</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> ("hello").multiply(3) =&gt; "hellohellohello"</FONT>
        <B>require</B>
            meaningful_multiplier: n &gt;= 1
</A>
    <A NAME="f_standard_copy"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_copy">standard_copy</A> (other: <A HREF="../base/string_8_flatshort.html">STRING_8</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy every field of </FONT>`other'<FONT COLOR="red"> onto corresponding field</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            other_not_void: other /= <B>Void</B>
            type_identity: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> (other)
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            is_standard_equal: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (other)
</A>
    <A NAME="f_standard_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_standard_twin">standard_twin</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object field-by-field identical to </FONT>`other'<FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Always uses default copying semantics.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            standard_twin_not_void: <B>Result</B> /= <B>Void</B>
            equal: <A HREF="../base/any_flatshort.html#f_standard_equal">standard_equal</A> (<B>Result</B>, <B>Current</B>)
</A>
    <A NAME="f_substring"><A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index, end_index: <A HREF="../base/integer_32_flatshort.html">INTEGER_32</A>): <B>like</B> <B>Current</B>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Copy of substring containing all characters at indices</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> between </FONT>`start_index'<FONT COLOR="red"> and </FONT>`end_index'
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_general_flatshort.html">READABLE_STRING_GENERAL</A>
            substring_not_void: <B>Result</B> /= <B>Void</B>
            substring_count: <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_count">count</A> = end_index - start_index + 1 <B>or</B> <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_count">count</A> = 0
            first_code: <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_count">count</A> &gt; 0 <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_code">code</A> (1) = <A HREF="../base/readable_string_8_flatshort.html#f_code">code</A> (start_index)
            recurse: <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_count">count</A> &gt; 0 <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_substring">substring</A> (2, <B>Result</B>.<A HREF="../base/readable_string_general_flatshort.html#f_count">count</A>).<A HREF="../base/comparable_flatshort.html#f_is_equal">is_equal</A> (<A HREF="../base/string_8_flatshort.html#f_substring">substring</A> (start_index + 1, end_index))
</A>
    <A NAME="f_twin"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_twin">twin</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New object equal to </FONT>`Current'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> </FONT><A HREF="../base/any_flatshort.html#f_twin">twin</A><FONT COLOR="red"> calls </FONT><A HREF="../base/readable_string_8_flatshort.html#f_copy">copy</A><FONT COLOR="red">; to change copying/twining semantics, redefine </FONT><A HREF="../base/readable_string_8_flatshort.html#f_copy">copy</A><FONT COLOR="red">.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            twin_not_void: <B>Result</B> /= <B>Void</B>
            is_equal: <B>Result</B>.<A HREF="../base/any_flatshort.html#f_is_equal">is_equal</A> (<B>Current</B>)
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Basic operations</FONT>

    <A NAME="f_default"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_default">default</A>: ?<A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Default value of object's type</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_default_pointer"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_default_pointer">default_pointer</A>: <A HREF="../base/pointer_flatshort.html">POINTER</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Default value of type </FONT>`POINTER'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Avoid the need to write </FONT>`p'<FONT COLOR="red">.</FONT><A HREF="../base/any_flatshort.html#f_default">default</A><FONT COLOR="red"> for</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> some </FONT>`p'<FONT COLOR="red"> of type </FONT>`POINTER'<FONT COLOR="red">.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_default_rescue"><A HREF="../base/any_flatshort.html#f_default_rescue">default_rescue</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Process exception for routines with no Rescue clause.</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> (Default: do nothing.)</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_do_nothing"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_do_nothing">do_nothing</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Execute a null action.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Correction</FONT>

    <A NAME="f_mismatch_information"><A HREF="../base/mismatch_corrector_flatshort.html#f_mismatch_information">mismatch_information</A>: <A HREF="../base/mismatch_information_flatshort.html">MISMATCH_INFORMATION</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Original attribute values of mismatched object</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/mismatch_corrector_flatshort.html">MISMATCH_CORRECTOR</A><FONT COLOR="red">)</FONT>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Output</FONT>

    <A NAME="f_io"><A HREF="../base/any_flatshort.html#f_io">io</A>: <A HREF="../base/std_files_flatshort.html">STD_FILES</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Handle to standard file setup</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            io_not_void: <B>Result</B> /= <B>Void</B>
</A>
    <A NAME="f_out"><A HREF="../base/readable_string_8_flatshort.html#f_out">out</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Printable representation</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A><FONT COLOR="red">)</FONT>
        <B>require</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT> <A HREF="../base/any_flatshort.html">ANY</A>
            <B>True</B>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            out_not_void: <B>Result</B> /= <B>Void</B>
        <B>ensure then</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
            out_not_void: <B>Result</B> /= <B>Void</B>
            same_items: <A HREF="../base/any_flatshort.html#f_same_type">same_type</A> ("") <B>implies</B> <B>Result</B>.<A HREF="../base/readable_string_8_flatshort.html#f_same_string">same_string</A> (<B>Current</B>)
</A>
    <A NAME="f_print"><A HREF="../base/any_flatshort.html#f_print">print</A> (some: ?<A HREF="../base/any_flatshort.html">ANY</A>)
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Write terse external representation of </FONT>`some'
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> on standard output.</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
</A>
    <A NAME="f_tagged_out"><B>frozen</B> <A HREF="../base/any_flatshort.html#f_tagged_out">tagged_out</A>: <A HREF="../base/string_8_flatshort.html">STRING_8</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> New string containing terse printable representation</FONT>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> of current object</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            tagged_out_not_void: <B>Result</B> /= <B>Void</B>
</A>    
<B>feature</B> <FONT COLOR="red">--</FONT><FONT COLOR="red"> Platform</FONT>

    <A NAME="f_operating_environment"><A HREF="../base/any_flatshort.html#f_operating_environment">operating_environment</A>: <A HREF="../base/operating_environment_flatshort.html">OPERATING_ENVIRONMENT</A>
            <FONT COLOR="red">--</FONT><FONT COLOR="red"> Objects available from the operating system</FONT>
            <FONT COLOR="red">--</FONT> <FONT COLOR="red">(from </FONT><A HREF="../base/any_flatshort.html">ANY</A><FONT COLOR="red">)</FONT>
        <B>ensure</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
            operating_environment_not_void: <B>Result</B> /= <B>Void</B>
</A>    
<B>invariant</B>
    extendible: <A HREF="../base/string_8_flatshort.html#f_extendible">extendible</A>
    compare_character: <B>not</B> <A HREF="../base/container_flatshort.html#f_object_comparison">object_comparison</A>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/readable_string_8_flatshort.html">READABLE_STRING_8</A>
    area_not_void: <A HREF="../base/string_8_flatshort.html#f_area">area</A> /= <B>Void</B>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/comparable_flatshort.html">COMPARABLE</A>
    irreflexive_comparison: <B>not</B> (<B>Current</B> &lt; <B>Current</B>)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/any_flatshort.html">ANY</A>
    reflexive_equality: <A HREF="../base/any_flatshort.html#f_standard_is_equal">standard_is_equal</A> (<B>Current</B>)
    reflexive_conformance: <A HREF="../base/any_flatshort.html#f_conforms_to">conforms_to</A> (<B>Current</B>)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/string_general_flatshort.html">STRING_GENERAL</A>
    mutable: <B>not</B> <A HREF="../base/readable_string_general_flatshort.html#f_is_immutable">is_immutable</A>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/indexable_flatshort.html">INDEXABLE</A>
    index_set_not_void: <A HREF="../base/readable_string_8_flatshort.html#f_index_set">index_set</A> /= <B>Void</B>

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/resizable_flatshort.html">RESIZABLE</A>
    increase_by_at_least_one: <A HREF="../base/resizable_flatshort.html#f_minimal_increase">minimal_increase</A> &gt;= 1

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/bounded_flatshort.html">BOUNDED</A>
    valid_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &lt;= <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>
    full_definition: <A HREF="../base/bounded_flatshort.html#f_full">full</A> = (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = <A HREF="../base/readable_string_8_flatshort.html#f_capacity">capacity</A>)

        <FONT COLOR="red">--</FONT> <FONT COLOR="red">from </FONT><A HREF="../base/finite_flatshort.html">FINITE</A>
    empty_definition: <A HREF="../base/finite_flatshort.html#f_is_empty">is_empty</A> = (<A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> = 0)
    non_negative_count: <A HREF="../base/readable_string_8_flatshort.html#f_count">count</A> &gt;= 0

<B>end</B> <FONT COLOR="red">--</FONT> <FONT COLOR="red">class </FONT><A HREF="../base/string_8_flatshort.html">STRING_8</A><TABLE BORDER="1" ALIGN="CENTER"><TR><TD><A HREF="../class_list.html">Classes</A></TD><TD><A HREF="../cluster_list.html">Clusters</A></TD><TD><A HREF="../cluster_hierarchy.html">Cluster hierarchy</A></TD><TD><A HREF="string_8_chart.html">Chart</A></TD><TD><A HREF="string_8_links.html">Relations</A></TD><TD>Flat contracts</TD></TR></TABLE></PRE>
<P ALIGN="CENTER"> &#045;&#045; Generated by ISE Eiffel &#045;&#045 </P>
<P ALIGN="CENTER">For more details: <A HREF="http://www.eiffel.com">www.eiffel.com</A></P>
</BODY>
</HTML>

